﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using ClearingRestartingAutomaton.Common;

namespace ClearingRestartingAutomaton.Base
{
    /// <summary>
    /// The AssumptionsInference class represents the core class for inferring 
    /// clearing restarting automaton based on positive and negative samples.
    /// </summary>
    [Serializable]
    public class AssumptionsInference
    {
        #region Constructors

        /// <summary>
        /// Default constructor of this class.
        /// </summary>
        public AssumptionsInference()
        {

        }

        #endregion

        #region Public Properties

        /// <summary>
        /// Gets the list of positive samples.
        /// </summary>
        public List<string> PositiveSamples
        {
            get { return this.positiveSamples; }
        }

        /// <summary>
        /// Gets the list of negative samples.
        /// </summary>
        public List<string> NegativeSamples
        {
            get { return this.negativeSamples; }
        }

        /// <summary>
        /// Log delegate.
        /// </summary>
        public Action<string> Log { get; set; }

        #endregion

        #region Public Methods

        /// <summary>
        /// Returns either the Automaton consistent with the given positive and negative samples
        /// having the specified maximal width of instructions and the length of contexts, or null.
        /// </summary>
        /// <param name="assumptions">Assumptions delegate.</param>
        /// <param name="maximalWidth">Maximal width of instructions.</param>
        /// <param name="contextLength">Length of contexts.</param>
        /// <returns>
        /// The instance of the Automaton class consistent with the given positive and negative samples.
        /// </returns>
        public Automaton GetAutomaton(Assumptions assumptions, int maximalWidth, int contextLength)
        {
            LogAppendLine("INFERENCE ALGORITHM STARTED AT " + DateTime.Now.ToString());

            SortedSet<string> positiveSampleSet = new SortedSet<string>(new StringLengthLexComparer());
            foreach (string positiveSample in this.PositiveSamples)
            {
                positiveSampleSet.Add(positiveSample);
            }

            InstructionCollection instrucionCollection = assumptions(this.PositiveSamples, maximalWidth, contextLength, Log);

            LogAppendLine("INFERRED " + instrucionCollection.Instructions.Count.ToString() + " ASSUMPTIONS: " +
                String.Join(", ", instrucionCollection.Instructions.Select(i => i.ToString())));

            SortedSet<string> usedNegativeSamples = new SortedSet<string>(new StringLengthLexComparer());

            List<Instruction> correctInstructionList = new List<Instruction>(instrucionCollection.Instructions.Count);
            foreach (Instruction instruction in instrucionCollection.Instructions)
            {
                bool correctInstruction = true;
                foreach (string negativeSample in this.NegativeSamples)
                {
                    InstructionStepCollection stepCollection = instruction.MakeStep(negativeSample, InstructionUse.Reduction);
                    foreach (InstructionStep step in stepCollection.Steps)
                    {
                        if (String.IsNullOrEmpty(step.ResultWord))
                        {
                            LogAppendLine("FILTERED " + instruction.ToString() + 
                                " DUE TO REDUCTION: " + negativeSample + " -> EMPTY WORD");
                            usedNegativeSamples.Add(negativeSample);
                            correctInstruction = false;
                            break;
                        }
                        else if (positiveSampleSet.Contains(step.ResultWord))
                        {
                            LogAppendLine("FILTERED " + instruction.ToString() +
                                " DUE TO REDUCTION: " + negativeSample + " -> " + step.ResultWord);
                            usedNegativeSamples.Add(negativeSample);
                            correctInstruction = false;
                            break;
                        }
                    }
                    if (!correctInstruction)
                    {
                        break;
                    }
                }
                if (correctInstruction)
                {
                    correctInstructionList.Add(instruction);
                }
            }

            LogAppendLine("USED " + usedNegativeSamples.Count.ToString() + " NEGATIVE SAMPLES: " +
                String.Join(", ", usedNegativeSamples));

            LogAppendLine("FOUND " + correctInstructionList.Count.ToString() + " CORRECT INSTRUCTIONS: " +
                String.Join(", ", correctInstructionList.Select(i => i.ToString())));

            Automaton automaton = new Automaton(correctInstructionList);
            automaton.Simplify();

            LogAppendLine("SIMPLIFICATION LEFT " + automaton.Instructions.Count.ToString() + " INSTRUCTIONS: " +
                String.Join(", ", automaton.Instructions.Select(i => i.ToString())));

            if (this.IsConsistent(automaton))
            {
                LogAppendLine("INFERENCE ALGORITHM FINISHED AT " + DateTime.Now.ToString());
                LogAppendLine("THE RESULTING AUTOMATON IS CONSISTENT:");
                LogAppend(automaton.ToString());
                return automaton;
            }
            else
            {
                LogAppendLine("INFERENCE ALGORITHM FINISHED AT " + DateTime.Now.ToString());
                LogAppendLine("THE RESULTING AUTOMATON IS NOT CONSISTENT:");
                LogAppend(automaton.ToString());
                return null;
            }
        }

        #endregion

        #region Private Methods

        private bool IsConsistent(Automaton automaton)
        {
            bool isConsistent = true;

            foreach (string positiveSample in this.PositiveSamples)
            {
                WordTree positiveClosure = automaton.MakeWordTree(
                    positiveSample,
                    StringDefaultValues.LeftDelimiter,
                    StringDefaultValues.RightDelimiter,
                    InstructionUse.Reduction, 0, 0);
                if (!positiveClosure.TreeSet.ContainsKey(String.Empty))
                {
                    LogAppendLine("THE POSITIVE SAMPLE " + positiveSample + " IS NOT REDUCIBLE TO THE EMPTY WORD");
                    isConsistent = false;
                }
            }

            foreach (string negativeSample in this.NegativeSamples)
            {
                WordTree negativeClosure = automaton.MakeWordTree(
                    negativeSample,
                    StringDefaultValues.LeftDelimiter,
                    StringDefaultValues.RightDelimiter,
                    InstructionUse.Reduction, 0, 0);
                if (negativeClosure.TreeSet.ContainsKey(String.Empty))
                {
                    LogAppendLine("THE NEGATIVE SAMPLE " + negativeSample + " IS REDUCIBLE TO THE EMPTY WORD");
                    isConsistent = false;
                }
                foreach (string positiveSample in this.PositiveSamples)
                {
                    if (negativeClosure.TreeSet.ContainsKey(positiveSample))
                    {
                        LogAppendLine("THE NEGATIVE SAMPLE " + negativeSample + " IS REDUCIBLE TO THE POSITIVE SAMPLE " + positiveSample);
                        isConsistent = false;
                    }
                }
            }

            return isConsistent;
        }

        private void LogAppend(string text)
        {
            if (this.Log != null)
            {
                this.Log(text);
            }
        }

        private void LogAppendLine(string text)
        {
            this.LogAppend(text + Environment.NewLine);
        }

        #endregion

        #region Private Data Members

        private List<string> positiveSamples = new List<string>();
        private List<string> negativeSamples = new List<string>();

        #endregion
    }
}
